'''
Created on 2011-5-19

@author: elm
'''


from ddbms.SqlParser import SqlBaseParser
import ddbms.RelationalAlgebra
from ddbms.DdbmsException import *

class Statement:
        'An SQL Query Statement'
        fieldrefs = []
        tablerefs = []
        condition = None
        def __init__(self,fields=[],tables=[],condition=None):
            self.fieldrefs=fields
            self.tablerefs=tables
            if(condition != None):
                self.condition=condition.toConjunction()
            else:
                self.condition=Conjunction()
                
        def __str__(self):
            str =       'SELECT  ' + ', '.join('%s' % id for id in self.fieldrefs)+'\n'
            str = str + 'FROM    ' + ', '.join('%s' % id for id in self.tablerefs)+'\n'
            if(self.condition!=None):
                str = str + 'WHERE   %s' % self.condition
            return str
        
class FieldRef:
        'Reference to a column in a table'
        table = None
        column = None
        segmentRef = False
        def __init__(self,table=None,column=None):
            self.table = table
            self.column = column
        def __str__(self):
            if(self.table==None):
                return  "_default.[%s]" % self.column
            else:
                return '%s.[%s]' %(self.table,self.column)        
        
        def __eq__(self,x):
            if(x==None):
                return False;
            else:
                return self.table==x.table and self.column==x.column
        
        def __ne__(self,x):
            if(x==None):
                return True;
            else:
                return self.table!=x.table or self.column!=x.column
            
class FieldRefAll(FieldRef):
        'Reference to all columns'
        def __str__(self):
            return '*'
        
class TableRef:
        'Reference to a table'        
        table = None
        def __init__(self,table=None):
            self.table=table
        def __str__(self):
            return '[%s]' % self.table
        
        def __eq__(self,x):
            if(x==None):
                return False;
            else:
                return self.table==x.table
        def __ne__(self,x):
            if(x==None):
                return True;
            else:
                return self.table!=x.table
class Condition:
        '"where" clause'
        def toConjunction(self):
            'convert a logical expression to a Conjunction form'
            return SqlStatement.Conjunction()
        def toCNF(self):
            'convert a logical expression to a CNF'
            
class CNF(Condition):
    "Conjunction Normal Form"
    conditions = None
    '''
    Type: List<List<Condition>
    The outer list is conjunction 
    and inner list is disjunction.
    Condition must be TestValue, TestField or their negative form
    i.e., [[a,b],[c,d,e]] means (a||b)&&(c||d||e) 
    '''
    def __init__(self,conditions=None):
        if conditions == None:
            self.conditions=[]
        else:
            self.conditions=conditions
    def __str__(self):
        ret = []
        for dnf in self.conditions:
            if len(dnf)>1:
                ret.append('(%s)'%(' OR '.join("%s" % s for s in dnf)))                
            else:
                ret.append(str(dnf[0]))
        return " AND ".join(ret)
    def toCNF(self):
        return self.minfied()
    
    def atomTest(self,atom,dict):
        atom = atom.toSimple()
        t1 = None
        op = None
        t2 = None
        if isinstance(atom,TestValue):
            k = "%s.%s"%(atom.fieldref.table.table,atom.fieldref.column)
            if k in dict:
                t1 = dict[k]
                op = atom.op
                t2 = atom.value
            else:
                return False
        elif isinstance(atom,TestField):
            k1 = "%s.%s"%(atom.leftfieldref.table.table,atom.leftfieldref.column)
            k2 = "%s.%s"%(atom.rightfieldref.table.table,atom.rightfieldref.column)
            if k1 in dict and k2 in dict:
                t1 = dict[k1]
                op = atom.op
                t2 = dict[k2]
        else:
            raise InvalidCondition
        if isinstance(t1,str):
            t1=t1.lower()
        if isinstance(t2,str):
            t2=t2.lower()
        if op == Ops.EQ:
            return t1 == t2
        elif op == Ops.NEQ:
            return t1 != t2
        elif op == Ops.LT:
            return t1 < t2
        elif op == Ops.LTEQ:
            return t1 <= t2
        elif op == Ops.GT:
            return t1 > t2
        elif op == Ops.GTEQ:
            return t1 >= t2
        else:
            raise InvalidOp
    def test(self,dict):
        '''
        Test if this CNF is true
        '''
        ret = True
        for dnf in self.conditions:
            dnftest = False
            for atom in dnf:
                dnftest = dnftest or self.atomTest(atom, dict)
                if dnftest:
                    break
            ret = ret and dnftest
            if not ret:
                break
        return ret
        
    def atomImply(self,atom1,atom2):
            '''
            determine if two atomic logical expression
            (i.e., TestValue,TestField and LogicalNot for them)
            has atomImply relation
            atom1 -> atom2
            '''
            atom1 = atom1.toSimple()
            atom2 = atom2.toSimple()
            if isinstance(atom2,TestField) and atom2.op == Ops.EQ and atom2.leftfieldref == atom2.rightfieldref:
                'atom2 always be true'
                return True
            if isinstance(atom1,TestValue) and isinstance(atom2,TestValue):
                if(atom1.fieldref != atom2.fieldref):
                    return False
                if atom2.op == Ops.EQ:
                    return atom1.op==Ops.EQ and atom1.value==atom2.value
                elif atom2.op == Ops.NEQ:
                    return ((atom1.op==Ops.NEQ and atom1.value==atom2.value)
                        or (atom1.op==Ops.LT and atom1.value <= atom2.value)
                        or (atom1.op==Ops.LTEQ and atom1.value < atom2.value)
                        or (atom1.op==Ops.GT and atom1.value >= atom2.value)
                        or (atom1.op==Ops.GTEQ and atom1.value > atom2.value)
                        or (atom1.op==Ops.EQ and atom1.value != atom2.value)
                        )
                elif atom2.op == Ops.LT:
                    return ((atom1.op==Ops.LT and atom1.value <= atom2.value)
                        or (atom1.op==Ops.LTEQ and atom1.value < atom2.value)
                        or (atom1.op==Ops.EQ and atom1.value < atom2.value)
                        )
                elif atom2.op == Ops.LTEQ: 
                    return ((atom1.op==Ops.LT and atom1.value <= atom2.value)
                        or (atom1.op==Ops.LTEQ and atom1.value <= atom2.value)
                        or (atom1.op==Ops.EQ and atom1.value <= atom2.value)
                        )
                elif atom2.op == Ops.GT: 
                    return ((atom1.op==Ops.GT and atom1.value >= atom2.value)
                        or (atom1.op==Ops.GTEQ and atom1.value > atom2.value)
                        or (atom1.op==Ops.EQ and atom1.value > atom2.value)
                        )
                elif atom2.op == Ops.GTEQ: 
                    return ((atom1.op==Ops.GT and atom1.value >= atom2.value)
                        or (atom1.op==Ops.GTEQ and atom1.value >= atom2.value)
                        or (atom1.op==Ops.EQ and atom1.value >= atom2.value)
                        )
                else:
                    raise InvalidOp                
            elif isinstance(atom1,TestField) and isinstance(atom2,TestField):
                if (atom1.leftfieldref != atom2.leftfieldref) or (atom1.rightfieldref != atom2.rightfieldref):
                    return False
                if atom1.op == atom2.op:
                    return True
                elif atom2.op == Ops.LTEQ:
                    return atom1.op == Ops.LT
                elif atom2.op == Ops.GTEQ:
                    return atom1.op == Ops.GT
                elif atom2.op == Ops.NEQ:
                    return atom1.op == Ops.LT or atom1.op == Ops.GT
                else:
                    return False
            else:
                return False
    def dnfImply(self,dnf1,dnf2):
        '''
        determine if two disjunction normal form
        have atomImply relation:
           (a|b) -> (c|d)
        <= (a->c | a->d) and (b->c or b->d) 
        '''
        for atom1 in dnf1:
            imp = False
            for atom2 in dnf2:
                imp = imp or self.atomImply(atom1, atom2)
            if not imp:
                return False
        return True
    
    def dnfConflict(self,dnf1,dnf2,rev=False):
            '''
            determine if two disjunction normal form
            is dnfConflict, e.g., can't be true simultaneously            
               (a|b) & (c|d|e) == False
            <= (a|b) -> !(c|d|e)
            <= (a|b) -> !c & (a|b) -> !d & (a|b) -> !e
            '''
            conf = True           
            for atom in dnf2:
                if not self.dnfImply(dnf1, [LogicalNot(atom).toSimple()]):
                    conf = False
                    break
            if conf:
                return True
            conf = True           
            for atom in dnf1:
                if not self.dnfImply(dnf2, [LogicalNot(atom).toSimple()]):
                    conf = False
                    break
            return conf
    def dnfMinfied(self,dnf):
        '''
        Remove redundancy expressions in a disjunction atomic form
        '''
        l = len(dnf)
        red = []
        for i in range(l):
            red.append(False)
        for i in range(l):
            for j in range(l):
                if i!=j and not red[i] and not red[j] and self.atomImply(dnf[i], dnf[j]):
                    red[i] = True
        min = []
        for i in range(l):
            if not red[i]:
                min.append(dnf[i])
        return min
        
            
    def minfied(self):
        '''
        Remove redundancy expressions:
        e.g.   a = 1 and [a = 1]
               a = a
               a < 1 and [a < 2]
        '''
        l = len(self.conditions)
        red = []
        for i in range(l):
            red.append(False)
            self.conditions[i] = self.dnfMinfied(self.conditions[i])
        for i in range(l):
            for j in range(l):
                if i!=j and not red[i] and not red[j] and self.dnfImply(self.conditions[i], self.conditions[j]):
                    red[j] = True
        min = []
        for i in range(l):
            if not red[i]:
                min.append(self.conditions[i]);
        return CNF(min)
    
    def sat(self):
        '''
        Determine whether this CNF is satisfiability.
        This is a typical NP-Complete problem.
        This algorithm is not an accuracy algorithm,
        just ensure that: sat=false -> SAT=false
        in which "sat" means this algorithm 
        and "SAT" is an accuracy algorithm.
        
           a & b & c == False
        <= a->!b or a->!c or a->
        '''
        
        l = len(self.conditions)
        for i in range(l-1):
            for j in range(i+1,l,1):
                if(self.dnfConflict(self.conditions[i],self.conditions[j])):
                    return False
        return True
        
class Conjunction(Condition):
        conditions = None
        def __init__(self,conditions=None):
            if conditions == None:
                self.conditions=[]
            else:
                self.conditions=conditions
        def __add__(self,x):
            return Conjunction(self.conditions+x.conditions)
        def __str__(self):
            return ' AND '.join('%s' % i for i in self.conditions)
        def toConjunction(self):
            return self
        def toCNF(self):
            cnf = []
            for cond in self.conditions:
                cnf += cond.toCNF().conditions
            return CNF(cnf).minfied()
        
class LogicalNot(Condition):
        condition = None
        def __init__(self,condition=None):
            self.condition=condition  
        def __str__(self):
            return '(NOT %s)'%self.condition      
        def toConjunction(self):
            if(type(self.condition)==LogicalOr):
                '!(a||b) == !a && !b'
                return Conjunction([
                    LogicalNot(self.condition.leftparam),
                    LogicalNot(self.condition.rightparam)
                ])
            else:
                return Conjunction([self])
        def toCNF(self):
            '''
              !((a|b)&(c|d|e)) 
            = !(a|b) | !(c|d|e)
            = (!a&!b) | (!c&!d&!e)
            = (!a|!c) & (!a|!d) & (!a|!e) & (!b|!c) & (!b|!d) & (!b|!e)
            '''
            neg = self.condition.toCNF().conditions
            ind = []
            ups = []
            l = len(neg)
            for dnf in neg:
                ind.append(0)
                ups.append(len(dnf))   
            cnf = []
            while True:
                dnf = []
                for i in range(l):
                    elem = neg[i][ind[i]]
                    if isinstance(elem,LogicalNot):
                        elem = elem.condition
                    else:
                        elem = LogicalNot(elem)
                    dnf.append(elem)
                cnf.append(dnf)
                ind[0]+=1
                for i in range(l-1):
                    while ind[i] >= ups[i]:
                        ind[i] = ind[i] - ups[i]
                        ind[i+1] += 1
                if ind[l-1] >= ups[l-1]:
                    break
            return CNF(cnf).minfied()
        def toSimple(self):
            '''
            Convert negative of TestValue and TestField 
            to their direct expression
            e.g., (not i < 1)  =>  (i >= 1) 
            '''
            if isinstance(self.condition,TestValue):
                return TestValue(self.condition.fieldref,
                                 self.condition.op.negative(), 
                                 self.condition.value)
            elif isinstance(self.condition,TestField):
                return TestField(self.condition.leftfieldref,
                                 self.condition.op.negative(), 
                                 self.condition.rightfieldref)
            elif isinstance(self.condition,LogicalNot):
                return self.condition.condition.toSimple()
            else:
                raise InvalidCondition
            
class LogicalAnd(Condition):
        leftparam = None
        rightparam = None
        def __init__(self,leftparam=None,rightparam=None):
            self.leftparam=leftparam
            self.rightparam=rightparam
        def __str__(self):
            return '(%s AND %s)'%(self.leftparam,self.rightparam)
        def toConjunction(self):
            return self.leftparam.toConjunction() + self.rightparam.toConjunction()
        def toCNF(self):
            lcnf = self.leftparam.toCNF().conditions
            rcnf = self.rightparam.toCNF().conditions
            return CNF(lcnf + rcnf).minfied()
            
class LogicalOr(Condition):
        leftparam = None
        rightparam = None
        def __init__(self,leftparam=None,rightparam=None):
            self.leftparam=leftparam
            self.rightparam=rightparam
        def __str__(self):
            return '(%s OR %s)'%(self.leftparam,self.rightparam)
        def toConjunction(self):
            return Conjunction([self])
        def toCNF(self):
            '''
              (a&b)|(c&d)
            = (a|c)&(a|d)&(b|c)&(b|d)
            '''
            lcnf = self.leftparam.toCNF().conditions
            rcnf = self.rightparam.toCNF().conditions
            li = 0
            ri = 0
            ll = len(lcnf)
            rl = len(rcnf)
            cnf = []
            while True:
                dnf = lcnf[li] + rcnf[ri]
                cnf.append(dnf)
                li += 1
                while li >= ll:
                    li -= ll
                    ri += 1
                if(ri >= rl):
                    break
            return CNF(cnf).minfied()
        
class TestValue(Condition):
        fieldref = None
        value = None
        op = None
        def __init__(self,fieldref=None,op=None,value=None):
            self.fieldref=fieldref
            self.op=op
            self.value=value 
        def __str__(self):
            return '%s %s %s'%(self.fieldref,self.op,self.value)
        
        def toConjunction(self):
            return Conjunction([self])
        def toCNF(self):
            return CNF([[self]])
        def toSimple(self):
            return self
            
class TestField(Condition):
        leftfieldref = None
        rightfieldref = None
        op = None
        def __init__(self,leftfieldref=None,op=None,rightfieldref=None):
            self.leftfieldref=leftfieldref
            self.op=op
            self.rightfieldref=rightfieldref    
        def __str__(self):
            return '%s %s %s'%(self.leftfieldref,self.op,self.rightfieldref)
        def toConjunction(self):
            return Conjunction([self])
        def toCNF(self):
            return CNF([[self]])
        def toSimple(self):
            return self
class Op:
    op = None
    
    def __init__(self,op=None):
        self.op = op
        
    def __str__(self):
        return self.op
    
    def __cmp__(self,x):
        return self.op==x.op
    
    def __eq__(self,x):
        return self.op==x.op
    
    def negative(self):
        op = self
        if op == Ops.EQ:
            return Ops.NEQ
        elif op == Ops.NEQ:
            return Ops.EQ
        elif op == Ops.LT:
            return Ops.GTEQ
        elif op == Ops.GTEQ:
            return Ops.LT
        elif op == Ops.GT:
            return Ops.LTEQ
        elif op == Ops.LTEQ:
            return Ops.GT 

class Ops:
    UNDEFINED = None
    
    AND = Op('AND')
    OR = Op('OR')
    NOT = Op('NOT')
    
    EQ = Op('=')
    NEQ = Op('<>')
    LT = Op('<')
    LTEQ = Op('<=')
    GT = Op('>')
    GTEQ = Op('>=')
    
    
    

class SqlStatement(SqlBaseParser):
    '''
    a parser which convert sql string to sql classes
    '''

    def ops(self,op):
        if(op=='<'):
            return Ops.LT
        elif(op=='='):
            return Ops.EQ
        elif(op=='>'):
            return Ops.GT
        elif(op=='<='):
            return Ops.LTEQ
        elif(op=='>='):
            return Ops.GTEQ
        elif(op=='<>'):
            return Ops.NEQ
        elif(op=='and'):
            return Ops.AND
        elif(op=='or'):
            return Ops.OR
        elif(op=='not'):
            return Ops.NOT
        else:
            return Ops.UNDEFINED 

    def statement(self,fieldrefs,tablerefs,where):
        'parse a sql statement'
        return Statement(fieldrefs,tablerefs,where)
    
    def tablerefs(self,refs):
        'parse "from" clause'
        return refs
    
    def tableref(self,table):
        'parse a table reference in "from" clause'
        return TableRef(table)
    
    def fieldrefs_all(self):  
        'parse star(*) in "select" clause'      
        return FieldRefAll()
    
    def fieldrefs(self,refs):
        'parse referred fields in "select" clause'
        return refs
        
    def fieldref(self,table,col):
        'parse a field reference'
        return FieldRef(table,col)      
    
    def condition_operation_binary(self,left,op,right):
        'binary operators (and, or)'
        if(op==Ops.AND):
            return LogicalAnd(left,right)
        elif(op==Ops.OR):
            return LogicalOr(left,right)
    
    def condition_operation_self(self,op,right):
        'unary operations (not)'
        return LogicalNot(right)
    
    def condition_value(self,fieldref,op,value):
        '''parse a condition clause 
           which compares a field and a value, i.e. x>1'''
        return TestValue(fieldref,op,value)
        
    def condition_field(self,leftfield,op,rightfield):
        '''parse a condition clause 
           which compares two fields, i.e. x>y'''
        return TestField(leftfield,op,rightfield)
    
    def value_number(self,v):
        'parse a number'  
        if(v.find('.')<0):
            return int(v)
        else:
            return float(v)
    
    def value_string(self,v):
        return str(v)   
    
